Daniel Cumming

Stay updated on KMIR's development progress as Runtime Verification defines the semantics of Rust's Middle Intermediate Representation (MIR) in the K Framework. Learn about Stable MIR serialization, the smir_pretty driver, and the future of KMIR's symbolic execution capabilities.

DALL·E 2024-09-13 03.23.10 - A flowchart-style diagram depicting the smir_pretty driver pipeline, showing connections between the Rust compiler and Stable MIR without any words or.webp

KMIR: Progress Update

Runtime Verification

Runtime Verification completed a design review of Lido's dual governance mechanism. This mechanism is the first of its kind, representing a monumental upgrade to the Lido governance model. This collaboration aimed to ensure that the new system, scheduled for testnet release in Q3 2024 and mainnet in Q4 2024, functions as intended and maintains the integrity and security of Lido’s $33 billion in total value locked (as of this writing). 


lido.png

With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review

Juan Conejero

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!


opt3 twitter.png

optimism

External Computation with Kontrol: <br/> Leveraging Foundry Execution for Formal Verification

Petar Maksimović

This is the second post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This installment explains how Kontrol can be used to tackle the complexities caused by dynamically-sized constructs and the challenges associated with the loops that result from them.

opt2 twitter.png

Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs

borderless-capital.png

Borderless Capital

fenbushi-capital.png

Fenbushi Capital

hypersphere-dark.png

hypersphere.png

Hypersphere

iosg-dark.png

iosg.png

IOSG

maven-11-dark.png

maven-11.png

Maven 11

multiversx-light.png

multiversx-dark.png

MultiversX

tezos-foundation-dark.png

tezos-foundation.png

Tezos Foundation (Investor)

wave-financial-dark.png

wave-financial.png

Wave Financial

alchemix.png

Alchemix

algorand-dark.png

algorand.png

Algorand

ashswap.png

AshSwap

band protocol white.png

band logo.png

Band Protocol

casper.png

Casper protocol

eigenlayer-dark.png

eigenlayer-light.png

EigenLayer

ethereum-logo-landscape-purple.png

Ethereum

folks-finance-dark.png

folks-finance.png

Folks Finance

hatom-dark.svg

hatom.svg

Hatom

HydraDX-Pink.png

HydraDX

Logo_lido.png

Lido

maker.png

Maker

membrane-dark.png

membrane.png

Membrane Finance

MORPHO.svg

Morpho-logo-black-horizontal.png

Morpho

nasa.png

NASA

olympus-dark.png

olympus.png

Olympus DAO

polkadot-dark.png

polkadot.png

Polkadot

stake.fish-dark.png

stake.fish.png

Stakefish

StakerDao-logo.png

StakerDAO

stakewise-dark.svg

stakewise.png

StakeWise

sundaeswap-dark.png

sundaeswap.png

SundaeSwap

swell-network.png

Swell Network

tezos.png

Tezos

Umee_Logo_dark_mode.png

Umee_Logo.png

Umee

Take Your Security to the Next Level

Start Verifying For Free

Formal Verification

K as a Service

Security Audits

Learn About Our Impact on Web3 Security

Categories

Partners & Customers

Investors

Testimonials

Contact Us